Search for: All records

Function Extraction (FX) is a new and evolving paradigm for the production of secure computer codes. It is, in effect, the inverse of formal verification as it analyzes code to produce a mathematical specification of its behavior. This has the potential for identifying unwanted or unexpected behaviors and has the potential for analyzing unknown or “found” code artifacts such as malware. The effort is enabled by recent developments in loop analysis that allow invariant relations to be developed for loop bodies enabling the loop function to be discovered. The paper defines program behavior as a mathematical description of the effects of program execution on the environment in which the program runs and continues with a discussion of its current status. As FX is an evolving paradigm, areas in which work remains to be done are discussed and examples of the results of two prototype analyzers are given. The paper concludes with a discussion of the path forward and the work that remains to be done. 

Abstract Invariant relations are used to analyze while loops; while their primary application is to derive the function of a loop, they can also be used to derive loop invariants, weakest preconditions, strongest postconditions, sufficient conditions of correctness, necessary conditions of correctness, and termination conditions of loops. In this paper we present two generic invariant relations that capture the semantics of loops whose loop body applies affine transformations on numeric variables.